

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%\paragraph{Correctness Properties: Bounded and Eventual Adaptation.~}
Here we define the correctness problems that we consider throughout the paper.
We would like adaptation properties defined in the most general way possible; 
this would allows us to analyze models of evolvable systems in different settings. 
For this purpose, 
our correctness properties are stated in terms of observability predicates, or  \emph{barbs}.
The definition of barbs is parameterized on the number of repetitions of a given signal.
We thus obtain a uniform definition for \emph{bounded} %\emph{single} 
 and \emph{repeated} weak  barbs.

\begin{definition}[Barbs]\label{d:barb}
Let $P$ be an $\mathcal{E}$ process, and let $\alpha$ be an action in $\{a, \outC{a} \mid a \in \mathcal{N}  \}$.
We write $P \downarrow_{\alpha}$ if there exists a $P'$ such that $P \arro{~\alpha~} P'$. Moreover:
\begin{itemize}
\item Given  $k > 0$, we write $P\barb{\alpha}^{k}$ 
%if there exists a computation 
iff there exist $Q_{1},\ldots, Q_{k}$ such that
$P \pired^{*} Q_1 \pired \ldots \pired Q_k$
with $Q_i \downarrow_\alpha$, for every $i \in \{1,\ldots, k\}$.
\item We write $P\barb{\alpha}^{\omega}$ iff
there exists an infinite computation
$P \pired^* Q_1 \pired Q_2 \pired  \ldots$
with $Q_i \downarrow_\alpha$ for every $i \in \mathbb{N}^+$.
\end{itemize}
Furthermore, we  use $\negbarbk{\alpha}$ and $\negbarbw{\alpha}$ to denote the negation of $\barbk{\alpha}$ and $\barbw{\alpha}$.
%, with the expected meaning.
\end{definition}

%% OLD VERSION OF BARBS
%%\todo{Controllare qui!!!!}
%\begin{definition}[Barbs]\label{d:barb}%and Reachability Problems
%Let $P$ be an $\mathcal{E}$ process, and let $\alpha$ be an action in $\{a, \outC{a} \mid a \in \mathcal{N}  \}$.
%We write $P \downarrow_{\alpha}$ if there exists a $P'$ such that $P \arro{~\alpha~} P'$.
%\begin{itemize}
%\item Given  $k > 0$, we write $P\barb{\alpha}^{k}$ 
%if there exists a computation $P = P_0 \pired \dots \pired P_l$  such that the cardinality of the set $\{j \in [0..l] \mid P_j \arro{~\alpha~} \}$  
%is greater than or equal to $k$.
%\item Analogously, we write $P\barb{\alpha}^{\omega}$ if there exist an infinite computation $P = P_0 \pired \dots \pired P_i \pired \dots$ such that  the set $\{j \in \mathbb{N} \mid P_j \arro{~\alpha~} \}$ is infinite.
%Furthermore,
% we use $\negbarbk{\alpha}$ and $\negbarbw{\alpha}$ to denote the negation of $\barbk{\alpha}$ and $\barbw{\alpha}$, with the expected meaning.
%\end{itemize}
%\end{definition}


We shall consider two instances of the problem of reaching an error configuration in an aggregation of terms, or \emph{cluster}.
%We consider three ways of defining clusters, or \emph{clustering schemas}, which are defined as process contexts.
%The first schema, \emph{standalone clustering},  defines the empty aggregation, that is, the context that considers a building block in isolation. 
%The second one, \emph{parallel clustering} admits the parallel composition of building blocks.
%%terms, and the repetition of the a single term can appear zero or more . 3. 
%Finally, \emph{updatable clusterings} extend parallel clusterings by allowing transparent localities in contexts.
%More formally, we have the following definition.
%\todo{Decidere terminologia: cosa mettere al posto di aggregation: deployment? clustering?}
A \emph{cluster} is a process obtained as the parallel composition of an initial process $P$
with an arbitrary set of processes $M$ representing its 
possible subsequent
modifications.
That is, 
processes in $M$
may contain update actions on the names of the adaptable processes  in $P$, 
and therefore may potentially lead to its modification (evolution).

\begin{definition}[Cluster] \label{d:cluster}
Let $P, P_1,\ldots,P_n$ 
be \evol{} processes and $M=\{P_1,\ldots,P_n\}$. 
%representing the possible subsequent modifications.
The set of clusters $\BC_P^M$ is defined as:
$$\BC_P^M = \big\{P \parallel \prod^{m_1} P_1 \parallel \dots \parallel \prod^{m_n} P_n \mid m_1, \dots, m_n \in \mathbb{N}\cup \{ 0 \} \big\}$$
\end{definition}

The  \emph{adaptation} problems 
below
%we are about to introduce 
formalize correctness of clusters
with respect to their ability for recovering from errors by means of update actions.
More precisely, 
given a set of clusters $\BC_P^M$
and a %distinguished 
barb $e$ (signaling an error), 
we would like to know if all computations of processes in $\BC_P^M$
\begin{enumerate}
\item have \underline{\emph{at most} $k$} consecutive states exhibiting $e$, or
\item have a \underline{\emph{finite}} number of consecutive states exhibiting $e$.
%\underline{\emph{eventually}} reach a state in which  $e$ is no longer 
%observable.
\end{enumerate}
We thus have the following definition:

\begin{definition}[Adaptation Problems]\label{def:adaptprob}
Suppose an initial process $P$,
a set of processes $M$, a barb $e$.

\begin{itemize}
\item  Given $k>0$, the \emph{bounded adaptation} problem (\OG) consists in checking  
whether for all  processes 
$R \in \BC_P^M$, $R \, \negbarbk{e}$ holds.

\item Similarly, the \emph{eventual adaptation} problem (\LG) consists in checking  
whether   
for all processes 
$R \in \BC_P^M$,  $R \, \negbarbw{e}$ holds.
\end{itemize}
\end{definition}

% OLD VERSION
%The  \emph{adaptation} properties we are about to introduce formalize correctness of clusters
%with respect to their ability for recovering from errors by means of evolvability actions.
%%in the presence of the evolvable behavior enforced by update actions. 
%More precisely, 
%given a set of clusters $\BC_P^M$
%and a distinguished barb $e$ (signaling an error), 
%we would like to know if all computations of processes in $\BC_P^M$
%(1) have \emph{at most} $k$ states that exhibit $e$, or
%(2) \emph{eventually} reach a state from which no other barbs on $e$ will be observed.
%
%\begin{definition}[Bounded and Eventual Adaptation]
%We define bounded and eventual adaptation as follows:
%\begin{itemize}
%\item The \emph{bounded adaptation} problem (\OG in the following) consists in checking  
%whether given an initial process $P$,
%a set of processes $M$, %=\{T_1, \dots,$ $T_n\}$, 
%a barb $e$,    
%and $k>0$, for all processes $R \in \BC_P^M$, $R \negbarbk{e}$ holds.
%\item  The \emph{eventual adaptation} problem (\LG in the following) consists in checking  
%whether given an initial process $P$,
%a set of processes $M$ and
%a barb $e$,    
%for all processes $R \in \BC_P^M$,  $R \negbarbw{e}$ holds.
% \end{itemize}
%\end{definition}

Similarly as processes, static clusters can be encoded into equivalent dynamic ones.


\begin{definition}
Let $P, P_{1},\ldots, P_{n}$ 
be \evols{} processes 
such that $M = \{P_1,\ldots,P_n\}$.
The static cluster set $\BC_P^M$ 
is transformed 
into a dynamic cluster set $\dyn{\BC_{P}^{M}}=\BC_{P'}^{M'}$ by taking $P' = \dyn{P}$ and $M' = \{\dyn{P_1},\ldots,\dyn{P_n}\}$, where $S = \CStrs(P) \cup \bigcup_{1 \leq i \leq n} \CStrs (P_i)$.
\end{definition}

\begin{theorem}\label{th:clusterstat}
Let $P, P_1,\ldots,P_n$ 
be \evols{} processes such that $M=\{P_1,\ldots,P_n\}$. 
Then 
%Given $P \in \evols{}$ and $M = \{P_1,\ldots,P_n\} \subset \evols{}$, 
we have
$\dyn{\BC_{P}^{M}} = \{ \dyn{C} \mid C \in \BC_{P}^{M} \}$, where $S = \CStrs(P) \cup \bigcup_{1 \leq i \leq n} \CStrs (P_i)$.
\end{theorem}
\begin{proof}
Immediate by observing that 
by Definition \ref{def:din},  
$\dyn{P}$ is an 
homomorphism with respect to parallel composition, i.e., $\dyn{P\parallel Q}= \dyn{P}\parallel \dyn{Q}$. 
\end{proof}



Notice that, for every cluster $C$ in $\dyn{\BC_{P}^{M}}$ 
by construction 
we have $\CStrs(C) \subseteq S$.
Hence, the operational correspondence given by  Theorem~\ref{stdynequiv} is individually applicable to each cluster.
